Inference at * 1 
Iof proof for Lemma integer sqrt:



1. n : 
  r:. (((r * r)  n) & (n < ((r+1) * (r+1)))) 

latex

 by InteriorProof NatInd 1 

latex

 1: .....basecase..... NILNIL

 1: (no hyps)
 1:   r:. (((r * r)  0) & (0 < ((r+1) * (r+1))))
 2: .....upcase..... NILNIL

 2: 1. n : 
 2: 2. 0 < n
 2: 3. r:. (((r * r)  (n - 1)) & ((n - 1) < ((r+1) * (r+1))))
 2:   r:. (((r * r)  n) & (n < ((r+1) * (r+1))))
 .

Definitions	n - m, n+m, -n, s = t, #$n, A, False, Void, x:A. B(x), P & Q, x:A  B(x), a < b, P  Q, x:A. B(x), x:AB(x), i  j , A  B, t  T, , {x:A| B(x)}
Lemmas	le wf, nat wf, ge wf, nat properties, nat ind tp